(declare-fun a () RoundingMode)
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Float64)
(assert (= ((_ to_fp 11 53) a 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0) c (fp.add a c d) b))
(check-sat)
(assert (= ((_ to_fp 11 53) a 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0) c (fp.add a c d) b))
(check-sat)
